Beyond foundation #751
Beyond foundation #751
Conversation
|
Ready for review |
|
Can we have #706 merged before this one? |
|
Not sure how this one didn't have any merge conflicts after your big refactor |
…on-equivalences-type-families-over-subuniverses to make the use of the word families in file names consistent, at least within the foundation folder
|
I made all the changes I wanted to make to integrate this well with #706. This one is now ready for review. |
|
Oh wait I want to make some more changes:) |
|
Now I think I got them all |
|
Great! I will review it this evening :) |
|
One other minor remark is, for completeness, we could also repeat all the computations for action on equivalences of type families over subuniverses, and in the process also create a file for action on equivalences of functions on subuniverses. |
|
Thanks for the review! I will work on it tonight! |
|
I addressed all your comments. Now it's a question of how much laws you want me to prove for the new actions on equivalences, and whether we want those laws that serve no immediate purpose to hold up the useful refactorings in this PR. |
|
None is fine. It was only a remark |
In this PR I pulled changes I made in the
foundationandfoundation-corefolders in the Beyond finite sets PR #623. The goal is to create something mergeable without having to wait for the other unfinished changes in #623. Let's see what monstrosity I created.